$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:ecl(${\it ds}$;${\it da}$), $m$:$\mathbb{N}$.
\\[0ex]ecl{-}act(${\it ds}$;${\it da}$;$m$;$x$) $\in$ (event{-}info(${\it ds}$;${\it da}$) List)$\rightarrow$Prop